Aritmética de função elementar
Em teoria da prova, que é um ramo da lógica matemática, aritmética de função elementar, também chamada de AFE (EFA), aritmética elementar ou aritmética de função exponencial, é o sistema da aritmética com propriedades elementares habituais de 0, 1, +, ×, xy, em conjunto com a indução para fórmulas com quantificadores limitados.
A AFE é um sistema lógico muito fraco, cujo ordinal da prova teórica é ω3, mas ainda parece ser capaz de provar muito da matemática ordinária que pode ser expressa em linguagem aritmética de primeira-ordem.
Definição
[editar | editar código-fonte]AFE é um sistema em lógica de primeira ordem (com igualdade). Sua linguagem contém:
- duas constantes 0, 1,
- três operações binárias +, ×, exp, com exp(x,y) normalmente escrita como xy,
- um símbolo de relação binária < (Isto não é realmente necessário já que ele pode ser escrito em termo das outras operações e é algumas vezes omitido, mas é conveniente para se definir quantificadores limitados).
Quantificadores limitados são aqueles na forma ∀(x<y) e ∃(x<y) que são abreviações para ∀x(x<y)→,,, e ∃x(x<y)∧... na maneira usual.
Os axiomas de AFE são
- Os axiomas da Aritmética de Robinson para 0, 1, +, ×, <
- Os axiomas para exponenciação: x0 = 1, xy+1 = xy×x.
- Indução para fórmulas cujos quantificadores são limitados (mas que podem conter variáveis livres).
Grande conjectura de Friedman
[editar | editar código-fonte]A grande conjectura de Harvey Friedman implica que muitos teoremas matemáticos, tal como o Último teorema de Fermat, podem ser provados em sistemas muito fracos como o AFE.
A declaração original da conjectura de Friedman (1999) é:
- "Todo teorema publicado nos Anais da Matemática cuja declaração envolve somente objetos matemáticos finitos (por exemplo, o que lógicos chamam de enunciado aritmético) pode ser provado em AFE. AFE é o fragmento fraco da Aritmética de Peano baseado nos usuais axiomas sem quantificadores para 0, 1, +, ×, exp, junto com o esquema de indução para todas as fórmulas na linguagem cujos quantificadores são limitados."
Enquanto é fácil construir enunciados aritméticos artificiais que são verdadeiros mas não têm prova em AFE, o objetivo da conjectura de Friedman é que exemplos naturais de tais enunciados na matemática parecem ser raros. Alguns exemplos naturais incluem enunciados de consistência provenientes da lógica, vários enunciados relacionados à Teoria de Ramsey tais como o lema da regularidade de Szemerédi e o teorema menor dos grafos, e o algoritmo de Tarjan para uma estrutura de dados de subconjuntos-disjuntos.
Sistemas relacionados
[editar | editar código-fonte]Pode-se omitir o símbolo exp de função binária da linguagem ao se tomar a artimética de Robinson junto com a indução de todas as fórmulas com quantificadores limitados e um axioma enunciando, grosso modo, que exponenciação é uma função definida em todos os lugares. Isto é similar ao AFE e tem a mesma força prova-teórica mas é mais complicado de se trabalhar.
Existem fragmentos fracos da aritmética de segunda ordem chamados RCA* 0 e WKL* 0 que têm a mesma força de consistência da AFE e são conservadores sobre ela por Π0 2 sentenças, o que é às vezes estudado em matemática reversa (Simpson 2009).
Aritmética recursiva elementar (ARE/ERA) é um subsistema da aritmética recursiva primitiva (ARP/PRA) onde a recursão é restrita a somas e produtos limitados. Isto também tem as mesmas Π0 2 sentenças que AFE, no sentido de que sempre que AFE prova ∀x∃y P(x,y), com P sendo livre de quantificadores, ARE prova a fórmula aberta P(x,T(x)), com T um termo definível em ARE.
Assim como PRA, ARE pode ser definida de maneira completamente livre de lógica, somente com as regras de substituição e de indução, e definindo equações para todas as funções recursivas elementares. No entanto, diferente de PRA, as funções recursivas elementares podem ser caracterizadas pelo fecho sob composição e projeção de um número finito de funções básicas, sendo assim, somente um número finito de equações definidoras é necessário.
Veja também
[editar | editar código-fonte]- ELEMENTARY, uma classe de complexidade computacional relacionada
- Hierarquia de Grzegorczyk
- Matemática reversa
- Problema algébrico colegial de Tarski
Referências
[editar | editar código-fonte]- Avigad, Jeremy (2003), «Number theory and elementary arithmetic», Philosophia Mathematica. Philosophy of Mathematics, its Learning, and its Application. Series III, ISSN 0031-8019, 11 (3): 257–284, MR 2006194, doi:10.1093/philmat/11.3.257
- Friedman, Harvey (1999), grand conjectures
- Simpson, Stephen G. (2009), Subsystems of second order arithmetic, ISBN 978-0-521-88439-6, Perspectives in Logic 2nd ed. , Cambridge University Press, MR 1723993